T:Type, f:(TT), m:(T).
(x:T. m(f(x))m(x) & (m(f(x)) = m(x)    f(x) = x))  (x:T. n:. f(f^n(x)) = f^n(x)) 

latex

Definitions	x:A. B(x), P & Q, AB, x:A. B(x), P  Q, Prop, , t  T, P  Q, f^n, ij, A, False, P  Q, P  Q, , Dec(P), {T}
Lemmas	fun exp add, decidable lt, fun exp add1 sub, fun exp wf, nat properties, ge wf, nat wf, le wf